ecl{-}machine3(${\it ds}$;${\it da}$;$x$;$T$;${\it ks}$;$a$;${\it snd}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$$l$$\in$remove{-}repeats(IdLnkDeq;msg{-}spec{-}links(${\it snd}$)).R{-}lnk{-}tags(${\it ds}$ $\oplus$ $x$ : $T$;${\it da}$;$l$;ecl{-}tags($l$;${\it snd}$);${\it ks}$;ecl{-}m3($a$;${\it snd}$;$x$;$l$))